package org.eclipse.iota.util;

import java.util.HashMap;
import java.util.Map;

import org.eclipse.emf.ecore.util.EcoreUtil;
import org.eclipse.iota.assignments.Assignment;
import org.eclipse.iota.model.Alternation;
import org.eclipse.iota.model.BinaryOperation;
import org.eclipse.iota.model.Boolean;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constant;
import org.eclipse.iota.model.Constraint;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.EquationType;
import org.eclipse.iota.model.Expression;
import org.eclipse.iota.model.Inclusion;
import org.eclipse.iota.model.MultiOperation;
import org.eclipse.iota.model.Negation;
import org.eclipse.iota.model.Property;
import org.eclipse.iota.model.Reference;
import org.eclipse.iota.model.UnaryOperation;
import org.eclipse.iota.model.Variable;

/**
 * Equality checking for Iota models. Equality is checked modulo:
 * <ul>
 * <li>Commutativity of <i>or</i>, <i>and</i>, +, *</li>
 * <li>Renaming of properties, sequents and variables</li>
 * </ul>
 * @author Christian Krause
 * @generated NOT
 */
public class IotaEqualityUtil {

	/**
	 * Check whether two properties are equal.
	 * @param p1 Property 1.
	 * @param p2 Property 2.
	 * @return <code>true</code> if they are equal.
	 */
	public static boolean equals(Property p1, Property p2) {
		
		// Check if they are the same:
		if (p1==p2) {
			return true;
		}
		
		// Compare the number of parameters, but not their names.
		if (p1.getParameters().size()!=p2.getParameters().size()) {
			return false;
		}
		
		// Compare the number of clauses.
		if (p1.getBody().getClauses().size()!=p2.getBody().getClauses().size()) {
			return false;
		}		
		
		// Copy the second alternation.
		Alternation a1 = p1.getBody();
		Alternation a2 = IotaCopyUtil.copy(p2.getBody());
		
		// Substitute all parameters in the copy.
		Assignment assignment = new Assignment();
		for (int i=0; i<p1.getParameters().size(); i++) {
			Variable v1 = p1.getParameters().get(i);
			Variable v2 = p2.getParameters().get(i);
			assignment.put(v2, v1);
		}
		new IotaVariableSubstituter(assignment).applyTo(a2);
		
		// Now check equality of the alternations:
		return equals(a1, a2);
		
	}

	/**
	 * Check whether two alternations are equal.
	 * @param a1 Alternation 1.
	 * @param a2 Alternation 2.
	 * @return <code>true</code> if they are equal.
	 */
	public static boolean equals(Alternation a1, Alternation a2) {
		
		// Check if they are the same.
		if (a1==a2) {
			return true;
		}
		
		// Compare the number of clauses.
		if (a1.getClauses().size()!=a2.getClauses().size()) {
			return false;
		}
		
		// Compare the clauses. The order does not matter!
		Map<Clause,Clause> map = new HashMap<Clause,Clause>();
		for (Clause c1 : a1.getClauses()) {
			for (Clause c2 : a2.getClauses()) {
				if (!map.containsValue(c2) && equals(c1, c2)) {
					map.put(c1, c2);
					break;
				}
			}
			if (!map.containsKey(c1)) {
				return false;
			}
		}
		
		// No reason why they shouldn't be equal.
		return true;
		
	}

	/**
	 * Check whether two clauses are equal.
	 * @param c1 Clause 1.
	 * @param c2 Clause 2.
	 * @return <code>true</code> if they are equal.
	 */
	public static boolean equals(Clause c1, Clause c2) {
		
		// Check if they are the same:
		if (c1==c2) {
			return true;
		}
		
		// Compare the number of existential quantifiers, but not their names.
		if (c1.getExistentials().size()!=c2.getExistentials().size()) {
			return false;
		}
		
		// Compare the number of constraints.
		if (c1.getConstraints().size()!=c2.getConstraints().size()) {
			return false;
		}
		
		// Copy the second clause because we need to modify it.
		c2 = IotaCopyUtil.copy(c2);
		
		// Substitute the existential quantifiers in the second clause.
		Assignment assignment = new Assignment();
		for (int i=0; i<c1.getExistentials().size(); i++) {
			Variable v1 = c1.getExistentials().get(i);
			Variable v2 = c2.getExistentials().get(i);
			assignment.put(v2, v1);
		}
		new IotaVariableSubstituter(assignment).applyTo(c2);
		
		// Compare the constraints. The order does not matter!
		Map<Constraint,Constraint> map = new HashMap<Constraint,Constraint>();
		for (Constraint g1 : c1.getConstraints()) {
			for (Constraint g2 : c2.getConstraints()) {
				if (!map.containsValue(g2) && equals(g1, g2)) {
					map.put(g1, g2);
					break;
				}
			}
			if (!map.containsKey(g1)) {
				return false;
			}
		}
		
		// No reason why they shouldn't be equal.
		return true;
		
	}

	/**
	 * Check if two constraints are equal.
	 * @param c1 Constraint 1.
	 * @param c2 Constraint 2.
	 * @return <code>true</code> if they are equals
	 */
	public static boolean equals(Constraint c1, Constraint c2) {
		
		// Equality check is done based on the constraint type.
		if (c1.eClass()!=c2.eClass()) {
			return false;
		}
		else if (c1 instanceof Equation) {
			return equals((Equation) c1, (Equation) c2);
		}
		else if (c1 instanceof Inclusion) {
			return equals((Inclusion) c1, (Inclusion) c2);
		}
		else if (c1 instanceof Boolean) {
			return equals((Boolean) c1, (Boolean) c2);
		}
		else {
			return EcoreUtil.equals(c1, c2); // fall-back (should not happen)
		}
		
	}

	/**
	 * Check whether to inclusions are equal.
	 * @param i1 Inclusion 1.
	 * @param i2 Inclusion 2.
	 * @return <code>true</code> if they are equal.
	 */
	public static boolean equals(Inclusion i1, Inclusion i2) {
		
		// Must refer to the same target property.
		if (i1.getTarget()!=i2.getTarget()) {
			return false;
		}
		
		// Compare number of arguments.
		if (i1.getArguments().size()!=i2.getArguments().size()) {
			return false;
		}
		
		// Compare the argument lists.
		int args = i1.getArguments().size();
		for (int i=0; i<args; i++) {
			if (i1.getArguments().get(i)!=i2.getArguments().get(i)) {
				return false;
			}
		}
		
		// No reason why they shouldn't be equal.
		return true;
		
	}	
	
	/**
	 * Check if two equations are equal.
	 * @param e1 Equation 1.
	 * @param e2 Equation 2.
	 * @return <code>true</code> if they are equal.
	 */
	public static boolean equals(Equation e1, Equation e2) {
		
		// Equation types.
		EquationType t1 = e1.getType();
		EquationType t2 = e2.getType();
		
		// Same type?
		if (t1==t2) {
			
			// Exactly the same?
			if (IotaEqualityUtil.equals(e1.getLeft(), e2.getLeft()) &&
				IotaEqualityUtil.equals(e1.getRight(), e2.getRight())) return true;
			
			// Special case: = and !=
			if (t1==EquationType.EQUAL || t1==EquationType.NOT_EQUAL) {
				if (IotaEqualityUtil.equals(e1.getLeft(), e2.getRight()) &&
					IotaEqualityUtil.equals(e1.getRight(), e2.getLeft())) return true;
			}
		}
		
		// Opposite type?
		if ((t1==EquationType.GREATER && t2==EquationType.LESS) ||
			(t2==EquationType.GREATER && t1==EquationType.LESS)) {
			if (IotaEqualityUtil.equals(e1.getLeft(), e2.getRight()) &&
				IotaEqualityUtil.equals(e1.getRight(), e2.getLeft())) return true;			
		}
		
		return false;
		
	}

	/**
	 * Check whether to booleans are equal.
	 * @param b1 Boolean 1.
	 * @param b2 Boolean 2.
	 * @return <code>true</code> if they are equal.
	 */
	public static boolean equals(Boolean b1, Boolean b2) {
		return b1.getValue()==b2.getValue();
	}

	
	/**
	 * Check whether two expressions are equal. This does not
	 * perform any simplifications or evaluations.
	 * @param e1 First expression.
	 * @param e2 Second expression.
	 * @return <code>true</code> if they are equal.
	 */
	public static boolean equals(Expression e1, Expression e2) {
		
		// Basic checks.
		if (e1==e2) return true;
		if (e1==null || e2==null) return false;
		
		// We have one special case: negative constants.
		if (e1 instanceof Negation && e2 instanceof Constant) {
			return equals(e2,e1);
		}
		if (e1 instanceof Constant && e2 instanceof Negation) {
			if (((Negation) e2).getOperand() instanceof Constant) {
				Constant c1 = (Constant) e1;
				Constant c2 = (Constant) ((Negation) e2).getOperand();
				return c1.copy().negate().isEqualTo(c2);
			}
		}
		
		// Now to the general case.
		if (e1.eClass()==e2.eClass()) {
			
			// Constants:
			if (e1 instanceof Constant) {
				return ((Constant) e1).getValue().equals(((Constant) e2).getValue());
			}
			
			// Variables:
			if (e1 instanceof Reference) {
				return (((Reference) e1).getVariable()==((Reference) e2).getVariable());
			}
			
			// Unary operations:
			if (e1 instanceof UnaryOperation) {
				UnaryOperation u1 = (UnaryOperation) e1;
				UnaryOperation u2 = (UnaryOperation) e2;
				return equals(u1.getOperand(),u2.getOperand());
			}
			
			// Binary operations:
			if (e1 instanceof BinaryOperation) {
				BinaryOperation b1 = (BinaryOperation) e1;
				BinaryOperation b2 = (BinaryOperation) e2;
				return equals(b1.getLeft(),b2.getLeft()) && equals(b1.getRight(),b2.getRight());
			}
			
			// Multi-operations.
			if (e1 instanceof MultiOperation) {
				MultiOperation m1 = (MultiOperation) e1;
				MultiOperation m2 = (MultiOperation) e2;
				if (m1.getOperands().size()!=m2.getOperands().size()) return false;
				for (Expression operand : m1.getOperands()) {
					int o1 = occurrences(operand, m1);
					int o2 = occurrences(operand, m2);
					if (o1!=o2) return false;
				}
				return true;
			}
			
			return EcoreUtil.equals(e1, e2);
		}
		return false;
	}

	/*
	 * Count the number of occurrences of an expression in a multi-operation.
	 */
	private static int occurrences(Expression expression, MultiOperation operation) {
		int occurrences = 0;
		for (Expression operand : operation.getOperands()) {
			if (equals(operand,expression)) occurrences++;
		}
		return occurrences;
	}

}
